Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(map_1,f),app(app(cons,h),t))  → app(app(cons,app(f,h)),app(app(map_1,f),t))
2:    app(app(app(map_2,f),c),app(app(cons,h),t))  → app(app(cons,app(app(f,h),c)),app(app(app(map_2,f),c),t))
3:    app(app(app(app(map_3,f),g),c),app(app(cons,h),t))  → app(app(cons,app(app(app(f,g),h),c)),app(app(app(app(map_3,f),g),c),t))
There are 15 dependency pairs:
4:    APP(app(map_1,f),app(app(cons,h),t))  → APP(app(cons,app(f,h)),app(app(map_1,f),t))
5:    APP(app(map_1,f),app(app(cons,h),t))  → APP(cons,app(f,h))
6:    APP(app(map_1,f),app(app(cons,h),t))  → APP(f,h)
7:    APP(app(map_1,f),app(app(cons,h),t))  → APP(app(map_1,f),t)
8:    APP(app(app(map_2,f),c),app(app(cons,h),t))  → APP(app(cons,app(app(f,h),c)),app(app(app(map_2,f),c),t))
9:    APP(app(app(map_2,f),c),app(app(cons,h),t))  → APP(cons,app(app(f,h),c))
10:    APP(app(app(map_2,f),c),app(app(cons,h),t))  → APP(app(f,h),c)
11:    APP(app(app(map_2,f),c),app(app(cons,h),t))  → APP(f,h)
12:    APP(app(app(map_2,f),c),app(app(cons,h),t))  → APP(app(app(map_2,f),c),t)
13:    APP(app(app(app(map_3,f),g),c),app(app(cons,h),t))  → APP(app(cons,app(app(app(f,g),h),c)),app(app(app(app(map_3,f),g),c),t))
14:    APP(app(app(app(map_3,f),g),c),app(app(cons,h),t))  → APP(cons,app(app(app(f,g),h),c))
15:    APP(app(app(app(map_3,f),g),c),app(app(cons,h),t))  → APP(app(app(f,g),h),c)
16:    APP(app(app(app(map_3,f),g),c),app(app(cons,h),t))  → APP(app(f,g),h)
17:    APP(app(app(app(map_3,f),g),c),app(app(cons,h),t))  → APP(f,g)
18:    APP(app(app(app(map_3,f),g),c),app(app(cons,h),t))  → APP(app(app(app(map_3,f),g),c),t)
The approximated dependency graph contains one SCC: {4,6-8,10-13,15,16,18}.
Tyrolean Termination Tool  (0.51 seconds)   ---  May 3, 2006